r:rationals. (qpositive(r))  ((qpositive(-(r)))) 

latex

Definitions	A, True, T, prop{i:l}, P  Q, P  Q, ff, tt, qinv(r), if b then t else f fi , t  T, qdiv(r; s), r * s, qpositive(r), P  Q, x:A. B(x), False, guard(T), P  Q, P  Q, nequal(T; a; b), A c B, int_nzero, x:A. B(x), subtype(S; T)
Lemmas	rationals wf, int inc rationals, qmul wf, qpositive wf, true wf, squash wf, not functionality wrt iff, assert of lt int, and functionality wrt iff, assert of band, or functionality wrt iff, assert of bor, iff transitivity, not wf, lt int wf, band wf, bor wf, assert wf, implies functionality wrt iff, int nzero properties, q-elim